InforLorV4, Main, Exploration, bibRecord, 001674

A Connection-based Characterization of Bi-intuitionistic Validity

Identifieur interne : 001674 ( Main/Exploration ); précédent : 001673; suivant : 001675

A Connection-based Characterization of Bi-intuitionistic Validity

Auteurs : Didier Galmiche [France] ; Daniel Méry [France]

Source :

Journal of Automated Reasoning [ 0168-7433 ] ; 2013-06-01.

RBID : ISTEX:9D81791BCABB6BB2835069FE5F29B9FA88DB3B50

Descripteurs français

Pascal (Inist)
- Arbre graphe, Calcul séquent, Digraphe, Graphe orienté, Logique intuitionniste, Logique propositionnelle, Modélisation, Multigraphe, Théorie graphe, Théorie preuve, Vérification programme.

English descriptors

KwdEn :
- Bi-intuitionistic logic, Connections, Counter-models, Digraph, Directed graph, Graph theory, Intuitionistic logic, Modeling, Multigraph, Program verification, Proof theory, Proof-search, Propositional logic, Resource graphs, Sequent calculus, Tree(graph).
mix :
- Bi-intuitionistic logic, Connections, Counter-models, Resource graphs , Proof-search.

Abstract

Abstract: We give a connection-based characterization of validity in propositional bi-intuitionistic logic in terms of specific directed graphs called R-graphs. Such a characterization is well-suited for deriving labelled proof-systems with counter-model construction facilities. We first define the notion of bi-intuitionistic R-graphs from which we then obtain a connection-based characterization of propositional bi-intuitionistic validity and derive a sound and complete cut-free free-variable labelled sequent calculus that enjoys variable splitting.

Url:

DOI: 10.1007/s10817-013-9279-4

Affiliations:

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Connection-based Characterization of Bi-intuitionistic Validity</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:9D81791BCABB6BB2835069FE5F29B9FA88DB3B50</idno>
<date when="2013" year="2013">2013</date>
<idno type="doi">10.1007/s10817-013-9279-4</idno>
<idno type="url">https://api.istex.fr/ark:/67375/VQC-LSRNGHHB-Q/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002488</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002488</idno>
<idno type="wicri:Area/Istex/Curation">002457</idno>
<idno type="wicri:Area/Istex/Checkpoint">000300</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000300</idno>
<idno type="wicri:doubleKey">0168-7433:2013:Galmiche D:a:connection:based</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01258963</idno>
<idno type="url">https://hal.archives-ouvertes.fr/hal-01258963</idno>
<idno type="wicri:Area/Hal/Corpus">000130</idno>
<idno type="wicri:Area/Hal/Curation">000130</idno>
<idno type="wicri:Area/Hal/Checkpoint">001399</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">001399</idno>
<idno type="wicri:doubleKey">0168-7433:2013:Galmiche D:a:connection:based</idno>
<idno type="wicri:Area/Main/Merge">001686</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:14-0018676</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000035</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000962</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000081</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000081</idno>
<idno type="wicri:doubleKey">0168-7433:2013:Galmiche D:a:connection:based</idno>
<idno type="wicri:Area/Main/Merge">001752</idno>
<idno type="wicri:Area/Main/Curation">001674</idno>
<idno type="wicri:Area/Main/Exploration">001674</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Connection-based Characterization of Bi-intuitionistic Validity</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>Université de Lorraine - LORIA, Campus Scientifique BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>Université de Lorraine - LORIA, Campus Scientifique BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Journal of Automated Reasoning</title>
<title level="j" type="abbrev">J Autom Reasoning</title>
<idno type="ISSN">0168-7433</idno>
<idno type="eISSN">1573-0670</idno>
<imprint><publisher>Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<date type="published" when="2013-06-01">2013-06-01</date>
<biblScope unit="volume">51</biblScope>
<biblScope unit="issue">1</biblScope>
<biblScope unit="page" from="3">3</biblScope>
<biblScope unit="page" to="26">26</biblScope>
</imprint>
<idno type="ISSN">0168-7433</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0168-7433</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Bi-intuitionistic logic</term>
<term>Connections</term>
<term>Counter-models</term>
<term>Digraph</term>
<term>Directed graph</term>
<term>Graph theory</term>
<term>Intuitionistic logic</term>
<term>Modeling</term>
<term>Multigraph</term>
<term>Program verification</term>
<term>Proof theory</term>
<term>Proof-search</term>
<term>Propositional logic</term>
<term>Resource graphs</term>
<term>Sequent calculus</term>
<term>Tree(graph)</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Arbre graphe</term>
<term>Calcul séquent</term>
<term>Digraphe</term>
<term>Graphe orienté</term>
<term>Logique intuitionniste</term>
<term>Logique propositionnelle</term>
<term>Modélisation</term>
<term>Multigraphe</term>
<term>Théorie graphe</term>
<term>Théorie preuve</term>
<term>Vérification programme</term>
</keywords>
<keywords scheme="mix" xml:lang="en"><term> Bi-intuitionistic logic</term>
<term> Connections</term>
<term> Counter-models</term>
<term> Resource graphs </term>
<term>Proof-search</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We give a connection-based characterization of validity in propositional bi-intuitionistic logic in terms of specific directed graphs called R-graphs. Such a characterization is well-suited for deriving labelled proof-systems with counter-model construction facilities. We first define the notion of bi-intuitionistic R-graphs from which we then obtain a connection-based characterization of propositional bi-intuitionistic validity and derive a sound and complete cut-free free-variable labelled sequent calculus that enjoys variable splitting.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Nancy</li>
<li>Vandœuvre-lès-Nancy</li>
</settlement>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</region>
<name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001674 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001674 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:9D81791BCABB6BB2835069FE5F29B9FA88DB3B50
   |texte=   A Connection-based Characterization of Bi-intuitionistic Validity
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

Serveur d'exploration sur la recherche en informatique en Lorraine

A Connection-based Characterization of Bi-intuitionistic Validity

A Connection-based Characterization of Bi-intuitionistic Validity

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.